Left Termination of the query pattern
qs(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 286 ms)
↳2 TRIPLES
↳3 UndefinedPredicateInTriplesTransformerProof (⇒, 0 ms)
↳4 TRIPLES
↳5 TriplesToPiDPProof (⇒, 542 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
    ↳9 PiDP
        ↳10 UsableRulesProof (⇔, 0 ms)
        ↳11 PiDP
        ↳12 PiDPToQDPProof (⇒, 0 ms)
        ↳13 QDP
        ↳14 QDPSizeChangeProof (⇔, 0 ms)
        ↳15 YES
    ↳16 PiDP
        ↳17 UsableRulesProof (⇔, 0 ms)
        ↳18 PiDP
        ↳19 PiDPToQDPProof (⇒, 0 ms)
        ↳20 QDP
        ↳21 QDPSizeChangeProof (⇔, 0 ms)
        ↳22 YES
    ↳23 PiDP
        ↳24 UsableRulesProof (⇔, 0 ms)
        ↳25 PiDP
        ↳26 PiDPToQDPProof (⇔, 0 ms)
        ↳27 QDP
        ↳28 QDPSizeChangeProof (⇔, 0 ms)
        ↳29 YES
    ↳30 PiDP
        ↳31 UsableRulesProof (⇔, 0 ms)
        ↳32 PiDP
        ↳33 PiDPToQDPProof (⇔, 0 ms)
        ↳34 QDP
        ↳35 QDPSizeChangeProof (⇔, 0 ms)
        ↳36 YES
    ↳37 PiDP
        ↳38 UsableRulesProof (⇔, 0 ms)
        ↳39 PiDP
        ↳40 PiDPToQDPProof (⇒, 0 ms)
        ↳41 QDP
        ↳42 QDPSizeChangeProof (⇔, 0 ms)
        ↳43 YES
    ↳44 PiDP
        ↳45 UsableRulesProof (⇔, 0 ms)
        ↳46 PiDP
        ↳47 PiDPToQDPProof (⇒, 19 ms)
        ↳48 QDP
        ↳49 QDPOrderProof (⇔, 226 ms)
        ↳50 QDP
        ↳51 DependencyGraphProof (⇔, 0 ms)
        ↳52 TRUE
    ↳53 PiDP
        ↳54 UsableRulesProof (⇔, 0 ms)
        ↳55 PiDP
        ↳56 PiDPToQDPProof (⇒, 0 ms)
        ↳57 QDP
        ↳58 QDPOrderProof (⇔, 139 ms)
        ↳59 QDP
        ↳60 DependencyGraphProof (⇔, 0 ms)
        ↳61 TRUE

(0) Obligation:

Clauses:

qs(.(X, Xs), Ys) :- ','(part(X, Xs, Littles, Bigs), ','(qs(Littles, Ls), ','(qs(Bigs, Bs), app(Ls, .(X, Bs), Ys)))).
qs([], []).
part(X, .(Y, Xs), .(Y, Ls), Bs) :- ','(gt(X, Y), part(X, Xs, Ls, Bs)).
part(X, .(Y, Xs), Ls, .(Y, Bs)) :- ','(le(X, Y), part(X, Xs, Ls, Bs)).
part(X, [], [], []).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).
app([], Ys, Ys).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(0), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(X)).
le(0, 0).

Query: qs(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

gtA(s(X1), s(X2)) :- gtA(X1, X2).
partB(X1, .(X2, X3), .(X2, X4), X5) :- gtA(X1, X2).
partB(X1, .(X2, X3), .(X2, X4), X5) :- ','(gtcA(X1, X2), partB(X1, X3, X4, X5)).
partB(X1, .(X2, X3), X4, .(X2, X5)) :- leC(X1, X2).
partB(X1, .(X2, X3), X4, .(X2, X5)) :- ','(lecC(X1, X2), partB(X1, X3, X4, X5)).
leC(s(X1), s(X2)) :- leC(X1, X2).
qsF(.(X1, X2), X3) :- partB(X1, X2, X4, X5).
qsF(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), qsF(X4, X6)).
qsF(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), ','(qscF(X4, X6), qsF(X5, X7))).
qsF(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), ','(qscF(X4, X6), ','(qscF(X5, X7), appI(X6, X1, X7, X3)))).
appI(.(X1, X2), X3, X4, .(X1, X5)) :- appI(X2, X3, X4, X5).
appG(.(X1, X2), X3, X4, .(X1, X5)) :- appG(X2, X3, X4, X5).
pE(X1, X2, X3, X4, X5) :- qsF(X1, X2).
pE(X1, X2, X3, X4, X5) :- ','(qscF(X1, X2), appG(X3, X4, X2, X5)).
qsD(.(X1, .(X2, X3)), X4) :- gtA(X1, X2).
qsD(.(X1, .(X2, X3)), X4) :- ','(gtcA(X1, X2), partB(X1, X3, X5, X6)).
qsD(.(X1, .(X2, X3)), X4) :- ','(gtcA(X1, X2), ','(partcB(X1, X3, X5, X6), qsD(.(X2, X5), X7))).
qsD(.(X1, .(X2, X3)), X4) :- ','(gtcA(X1, X2), ','(partcB(X1, X3, X5, X6), ','(qscD(.(X2, X5), X7), pE(X6, X8, X7, X1, X4)))).
qsD(.(X1, .(X2, X3)), X4) :- leC(X1, X2).
qsD(.(X1, .(X2, X3)), X4) :- ','(lecC(X1, X2), partB(X1, X3, X5, X6)).
qsD(.(X1, .(X2, X3)), X4) :- ','(lecC(X1, X2), ','(partcB(X1, X3, X5, X6), qsF(X5, X7))).
qsD(.(X1, .(X2, X3)), X4) :- ','(lecC(X1, X2), ','(partcB(X1, X3, X5, X6), ','(qscF(X5, X7), pE(.(X2, X6), X8, X7, X1, X4)))).
qsD(.(X1, []), X2) :- qsH(X3).
qsD(.(X1, []), X2) :- ','(qscH(X3), qsH(X4)).
qsD(.(X1, []), X2) :- ','(qscH(X3), ','(qscH(X4), appG(X3, X1, X4, X2))).

Clauses:

gtcA(s(X1), s(X2)) :- gtcA(X1, X2).
gtcA(s(0), 0).
partcB(X1, .(X2, X3), .(X2, X4), X5) :- ','(gtcA(X1, X2), partcB(X1, X3, X4, X5)).
partcB(X1, .(X2, X3), X4, .(X2, X5)) :- ','(lecC(X1, X2), partcB(X1, X3, X4, X5)).
partcB(X1, [], [], []).
lecC(s(X1), s(X2)) :- lecC(X1, X2).
lecC(0, s(X1)).
lecC(0, 0).
qscD(.(X1, .(X2, X3)), X4) :- ','(gtcA(X1, X2), ','(partcB(X1, X3, X5, X6), ','(qscD(.(X2, X5), X7), qcE(X6, X8, X7, X1, X4)))).
qscD(.(X1, .(X2, X3)), X4) :- ','(lecC(X1, X2), ','(partcB(X1, X3, X5, X6), ','(qscF(X5, X7), qcE(.(X2, X6), X8, X7, X1, X4)))).
qscD(.(X1, []), X2) :- ','(qscH(X3), ','(qscH(X4), appcG(X3, X1, X4, X2))).
qscD([], []).
qscF(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), ','(qscF(X4, X6), ','(qscF(X5, X7), appcI(X6, X1, X7, X3)))).
qscF([], []).
appcI(.(X1, X2), X3, X4, .(X1, X5)) :- appcI(X2, X3, X4, X5).
appcI([], X1, X2, .(X1, X2)).
appcG(.(X1, X2), X3, X4, .(X1, X5)) :- appcG(X2, X3, X4, X5).
appcG([], X1, X2, .(X1, X2)).
qcE(X1, X2, X3, X4, X5) :- ','(qscF(X1, X2), appcG(X3, X4, X2, X5)).
qscH([]).

Afs:

qsD(x1, x2)  =  qsD(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [DT09].

(4) Obligation:

Triples:

gtA(s(X1), s(X2)) :- gtA(X1, X2).
partB(X1, .(X2, X3), .(X2, X4), X5) :- gtA(X1, X2).
partB(X1, .(X2, X3), .(X2, X4), X5) :- ','(gtcA(X1, X2), partB(X1, X3, X4, X5)).
partB(X1, .(X2, X3), X4, .(X2, X5)) :- leC(X1, X2).
partB(X1, .(X2, X3), X4, .(X2, X5)) :- ','(lecC(X1, X2), partB(X1, X3, X4, X5)).
leC(s(X1), s(X2)) :- leC(X1, X2).
qsF(.(X1, X2), X3) :- partB(X1, X2, X4, X5).
qsF(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), qsF(X4, X6)).
qsF(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), ','(qscF(X4, X6), qsF(X5, X7))).
qsF(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), ','(qscF(X4, X6), ','(qscF(X5, X7), appI(X6, X1, X7, X3)))).
appI(.(X1, X2), X3, X4, .(X1, X5)) :- appI(X2, X3, X4, X5).
appG(.(X1, X2), X3, X4, .(X1, X5)) :- appG(X2, X3, X4, X5).
pE(X1, X2, X3, X4, X5) :- qsF(X1, X2).
pE(X1, X2, X3, X4, X5) :- ','(qscF(X1, X2), appG(X3, X4, X2, X5)).
qsD(.(X1, .(X2, X3)), X4) :- gtA(X1, X2).
qsD(.(X1, .(X2, X3)), X4) :- ','(gtcA(X1, X2), partB(X1, X3, X5, X6)).
qsD(.(X1, .(X2, X3)), X4) :- ','(gtcA(X1, X2), ','(partcB(X1, X3, X5, X6), qsD(.(X2, X5), X7))).
qsD(.(X1, .(X2, X3)), X4) :- ','(gtcA(X1, X2), ','(partcB(X1, X3, X5, X6), ','(qscD(.(X2, X5), X7), pE(X6, X8, X7, X1, X4)))).
qsD(.(X1, .(X2, X3)), X4) :- leC(X1, X2).
qsD(.(X1, .(X2, X3)), X4) :- ','(lecC(X1, X2), partB(X1, X3, X5, X6)).
qsD(.(X1, .(X2, X3)), X4) :- ','(lecC(X1, X2), ','(partcB(X1, X3, X5, X6), qsF(X5, X7))).
qsD(.(X1, .(X2, X3)), X4) :- ','(lecC(X1, X2), ','(partcB(X1, X3, X5, X6), ','(qscF(X5, X7), pE(.(X2, X6), X8, X7, X1, X4)))).
qsD(.(X1, []), X2) :- ','(qscH(X3), ','(qscH(X4), appG(X3, X1, X4, X2))).

Clauses:

gtcA(s(X1), s(X2)) :- gtcA(X1, X2).
gtcA(s(0), 0).
partcB(X1, .(X2, X3), .(X2, X4), X5) :- ','(gtcA(X1, X2), partcB(X1, X3, X4, X5)).
partcB(X1, .(X2, X3), X4, .(X2, X5)) :- ','(lecC(X1, X2), partcB(X1, X3, X4, X5)).
partcB(X1, [], [], []).
lecC(s(X1), s(X2)) :- lecC(X1, X2).
lecC(0, s(X1)).
lecC(0, 0).
qscD(.(X1, .(X2, X3)), X4) :- ','(gtcA(X1, X2), ','(partcB(X1, X3, X5, X6), ','(qscD(.(X2, X5), X7), qcE(X6, X8, X7, X1, X4)))).
qscD(.(X1, .(X2, X3)), X4) :- ','(lecC(X1, X2), ','(partcB(X1, X3, X5, X6), ','(qscF(X5, X7), qcE(.(X2, X6), X8, X7, X1, X4)))).
qscD(.(X1, []), X2) :- ','(qscH(X3), ','(qscH(X4), appcG(X3, X1, X4, X2))).
qscD([], []).
qscF(.(X1, X2), X3) :- ','(partcB(X1, X2, X4, X5), ','(qscF(X4, X6), ','(qscF(X5, X7), appcI(X6, X1, X7, X3)))).
qscF([], []).
appcI(.(X1, X2), X3, X4, .(X1, X5)) :- appcI(X2, X3, X4, X5).
appcI([], X1, X2, .(X1, X2)).
appcG(.(X1, X2), X3, X4, .(X1, X5)) :- appcG(X2, X3, X4, X5).
appcG([], X1, X2, .(X1, X2)).
qcE(X1, X2, X3, X4, X5) :- ','(qscF(X1, X2), appcG(X3, X4, X2, X5)).
qscH([]).

Afs:

qsD(x1, x2)  =  qsD(x1)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
qsD_in: (b,f)
gtA_in: (b,b)
gtcA_in: (b,b)
partB_in: (b,b,f,f)
leC_in: (b,b)
lecC_in: (b,b)
partcB_in: (b,b,f,f)
qsF_in: (b,f)
qscF_in: (b,f)
appcI_in: (b,b,b,f)
appI_in: (b,b,b,f)
pE_in: (b,f,b,b,f)
appG_in: (b,b,b,f)
qscD_in: (b,f)
qcE_in: (b,f,b,b,f)
appcG_in: (b,b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

QSD_IN_GA(.(X1, .(X2, X3)), X4) → U21_GA(X1, X2, X3, X4, gtA_in_gg(X1, X2))
QSD_IN_GA(.(X1, .(X2, X3)), X4) → GTA_IN_GG(X1, X2)
GTA_IN_GG(s(X1), s(X2)) → U1_GG(X1, X2, gtA_in_gg(X1, X2))
GTA_IN_GG(s(X1), s(X2)) → GTA_IN_GG(X1, X2)
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U22_GA(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U23_GA(X1, X2, X3, X4, partB_in_ggaa(X1, X3, X5, X6))
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X5, X6)
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U2_GGAA(X1, X2, X3, X4, X5, gtA_in_gg(X1, X2))
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → GTA_IN_GG(X1, X2)
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U4_GGAA(X1, X2, X3, X4, X5, partB_in_ggaa(X1, X3, X4, X5))
U3_GGAA(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → U5_GGAA(X1, X2, X3, X4, X5, leC_in_gg(X1, X2))
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → LEC_IN_GG(X1, X2)
LEC_IN_GG(s(X1), s(X2)) → U8_GG(X1, X2, leC_in_gg(X1, X2))
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → U6_GGAA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U6_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U7_GGAA(X1, X2, X3, X4, X5, partB_in_ggaa(X1, X3, X4, X5))
U6_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U24_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U25_GA(X1, X2, X3, X4, qsD_in_ga(.(X2, X5), X7))
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSD_IN_GA(.(X2, X5), X7)
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U28_GA(X1, X2, X3, X4, leC_in_gg(X1, X2))
QSD_IN_GA(.(X1, .(X2, X3)), X4) → LEC_IN_GG(X1, X2)
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U29_GA(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U29_GA(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U30_GA(X1, X2, X3, X4, partB_in_ggaa(X1, X3, X5, X6))
U29_GA(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X5, X6)
U29_GA(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U31_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U31_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U32_GA(X1, X2, X3, X4, qsF_in_ga(X5, X7))
U31_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSF_IN_GA(X5, X7)
QSF_IN_GA(.(X1, X2), X3) → U9_GA(X1, X2, X3, partB_in_ggaa(X1, X2, X4, X5))
QSF_IN_GA(.(X1, X2), X3) → PARTB_IN_GGAA(X1, X2, X4, X5)
QSF_IN_GA(.(X1, X2), X3) → U10_GA(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U11_GA(X1, X2, X3, qsF_in_ga(X4, X6))
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → QSF_IN_GA(X4, X6)
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U12_GA(X1, X2, X3, X5, qscF_in_ga(X4, X6))
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U13_GA(X1, X2, X3, qsF_in_ga(X5, X7))
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → QSF_IN_GA(X5, X7)
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U14_GA(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U14_GA(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U15_GA(X1, X2, X3, appI_in_ggga(X6, X1, X7, X3))
U14_GA(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → APPI_IN_GGGA(X6, X1, X7, X3)
APPI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U16_GGGA(X1, X2, X3, X4, X5, appI_in_ggga(X2, X3, X4, X5))
APPI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPI_IN_GGGA(X2, X3, X4, X5)
U31_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U33_GA(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U33_GA(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U34_GA(X1, X2, X3, X4, pE_in_gagga(.(X2, X6), X8, X7, X1, X4))
U33_GA(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → PE_IN_GAGGA(.(X2, X6), X8, X7, X1, X4)
PE_IN_GAGGA(X1, X2, X3, X4, X5) → U18_GAGGA(X1, X2, X3, X4, X5, qsF_in_ga(X1, X2))
PE_IN_GAGGA(X1, X2, X3, X4, X5) → QSF_IN_GA(X1, X2)
PE_IN_GAGGA(X1, X2, X3, X4, X5) → U19_GAGGA(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U19_GAGGA(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U20_GAGGA(X1, X2, X3, X4, X5, appG_in_ggga(X3, X4, X2, X5))
U19_GAGGA(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → APPG_IN_GGGA(X3, X4, X2, X5)
APPG_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U17_GGGA(X1, X2, X3, X4, X5, appG_in_ggga(X2, X3, X4, X5))
APPG_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPG_IN_GGGA(X2, X3, X4, X5)
QSD_IN_GA(.(X1, []), X2) → U35_GA(X1, X2, qscH_in_a(X3))
U35_GA(X1, X2, qscH_out_a(X3)) → U36_GA(X1, X2, X3, qscH_in_a(X4))
U36_GA(X1, X2, X3, qscH_out_a(X4)) → U37_GA(X1, X2, appG_in_ggga(X3, X1, X4, X2))
U36_GA(X1, X2, X3, qscH_out_a(X4)) → APPG_IN_GGGA(X3, X1, X4, X2)
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U26_GA(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
U26_GA(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U27_GA(X1, X2, X3, X4, pE_in_gagga(X6, X8, X7, X1, X4))
U26_GA(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → PE_IN_GAGGA(X6, X8, X7, X1, X4)

The TRS R consists of the following rules:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
qsD_in_ga(x1, x2)  =  qsD_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
gtA_in_gg(x1, x2)  =  gtA_in_gg(x1, x2)
s(x1)  =  s(x1)
gtcA_in_gg(x1, x2)  =  gtcA_in_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
0  =  0
gtcA_out_gg(x1, x2)  =  gtcA_out_gg(x1, x2)
partB_in_ggaa(x1, x2, x3, x4)  =  partB_in_ggaa(x1, x2)
leC_in_gg(x1, x2)  =  leC_in_gg(x1, x2)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U40_ggaa(x1, x2, x3, x4, x5, x6)  =  U40_ggaa(x1, x2, x3, x6)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qsF_in_ga(x1, x2)  =  qsF_in_ga(x1)
qscF_in_ga(x1, x2)  =  qscF_in_ga(x1)
U56_ga(x1, x2, x3, x4)  =  U56_ga(x1, x2, x4)
U57_ga(x1, x2, x3, x4, x5)  =  U57_ga(x1, x2, x4, x5)
qscF_out_ga(x1, x2)  =  qscF_out_ga(x1, x2)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4)  =  U59_ga(x1, x2, x4)
appcI_in_ggga(x1, x2, x3, x4)  =  appcI_in_ggga(x1, x2, x3)
U60_ggga(x1, x2, x3, x4, x5, x6)  =  U60_ggga(x1, x2, x3, x4, x6)
appcI_out_ggga(x1, x2, x3, x4)  =  appcI_out_ggga(x1, x2, x3, x4)
appI_in_ggga(x1, x2, x3, x4)  =  appI_in_ggga(x1, x2, x3)
pE_in_gagga(x1, x2, x3, x4, x5)  =  pE_in_gagga(x1, x3, x4)
appG_in_ggga(x1, x2, x3, x4)  =  appG_in_ggga(x1, x2, x3)
qscH_in_a(x1)  =  qscH_in_a
qscH_out_a(x1)  =  qscH_out_a(x1)
qscD_in_ga(x1, x2)  =  qscD_in_ga(x1)
U45_ga(x1, x2, x3, x4, x5)  =  U45_ga(x1, x2, x3, x5)
U46_ga(x1, x2, x3, x4, x5)  =  U46_ga(x1, x2, x3, x5)
U47_ga(x1, x2, x3, x4, x5, x6)  =  U47_ga(x1, x2, x3, x5, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
qcE_in_gagga(x1, x2, x3, x4, x5)  =  qcE_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
appcG_in_ggga(x1, x2, x3, x4)  =  appcG_in_ggga(x1, x2, x3)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
appcG_out_ggga(x1, x2, x3, x4)  =  appcG_out_ggga(x1, x2, x3, x4)
qcE_out_gagga(x1, x2, x3, x4, x5)  =  qcE_out_gagga(x1, x2, x3, x4, x5)
qscD_out_ga(x1, x2)  =  qscD_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
U54_ga(x1, x2, x3, x4)  =  U54_ga(x1, x3, x4)
U55_ga(x1, x2, x3)  =  U55_ga(x1, x3)
U48_ga(x1, x2, x3, x4, x5)  =  U48_ga(x1, x2, x3, x5)
QSD_IN_GA(x1, x2)  =  QSD_IN_GA(x1)
U21_GA(x1, x2, x3, x4, x5)  =  U21_GA(x1, x2, x3, x5)
GTA_IN_GG(x1, x2)  =  GTA_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x1, x2, x3)
U22_GA(x1, x2, x3, x4, x5)  =  U22_GA(x1, x2, x3, x5)
U23_GA(x1, x2, x3, x4, x5)  =  U23_GA(x1, x2, x3, x5)
PARTB_IN_GGAA(x1, x2, x3, x4)  =  PARTB_IN_GGAA(x1, x2)
U2_GGAA(x1, x2, x3, x4, x5, x6)  =  U2_GGAA(x1, x2, x3, x6)
U3_GGAA(x1, x2, x3, x4, x5, x6)  =  U3_GGAA(x1, x2, x3, x6)
U4_GGAA(x1, x2, x3, x4, x5, x6)  =  U4_GGAA(x1, x2, x3, x6)
U5_GGAA(x1, x2, x3, x4, x5, x6)  =  U5_GGAA(x1, x2, x3, x6)
LEC_IN_GG(x1, x2)  =  LEC_IN_GG(x1, x2)
U8_GG(x1, x2, x3)  =  U8_GG(x1, x2, x3)
U6_GGAA(x1, x2, x3, x4, x5, x6)  =  U6_GGAA(x1, x2, x3, x6)
U7_GGAA(x1, x2, x3, x4, x5, x6)  =  U7_GGAA(x1, x2, x3, x6)
U24_GA(x1, x2, x3, x4, x5)  =  U24_GA(x1, x2, x3, x5)
U25_GA(x1, x2, x3, x4, x5)  =  U25_GA(x1, x2, x3, x5)
U28_GA(x1, x2, x3, x4, x5)  =  U28_GA(x1, x2, x3, x5)
U29_GA(x1, x2, x3, x4, x5)  =  U29_GA(x1, x2, x3, x5)
U30_GA(x1, x2, x3, x4, x5)  =  U30_GA(x1, x2, x3, x5)
U31_GA(x1, x2, x3, x4, x5)  =  U31_GA(x1, x2, x3, x5)
U32_GA(x1, x2, x3, x4, x5)  =  U32_GA(x1, x2, x3, x5)
QSF_IN_GA(x1, x2)  =  QSF_IN_GA(x1)
U9_GA(x1, x2, x3, x4)  =  U9_GA(x1, x2, x4)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
U11_GA(x1, x2, x3, x4)  =  U11_GA(x1, x2, x4)
U12_GA(x1, x2, x3, x4, x5)  =  U12_GA(x1, x2, x4, x5)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x2, x4)
U14_GA(x1, x2, x3, x4, x5)  =  U14_GA(x1, x2, x4, x5)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x2, x4)
APPI_IN_GGGA(x1, x2, x3, x4)  =  APPI_IN_GGGA(x1, x2, x3)
U16_GGGA(x1, x2, x3, x4, x5, x6)  =  U16_GGGA(x1, x2, x3, x4, x6)
U33_GA(x1, x2, x3, x4, x5, x6)  =  U33_GA(x1, x2, x3, x5, x6)
U34_GA(x1, x2, x3, x4, x5)  =  U34_GA(x1, x2, x3, x5)
PE_IN_GAGGA(x1, x2, x3, x4, x5)  =  PE_IN_GAGGA(x1, x3, x4)
U18_GAGGA(x1, x2, x3, x4, x5, x6)  =  U18_GAGGA(x1, x3, x4, x6)
U19_GAGGA(x1, x2, x3, x4, x5, x6)  =  U19_GAGGA(x1, x3, x4, x6)
U20_GAGGA(x1, x2, x3, x4, x5, x6)  =  U20_GAGGA(x1, x3, x4, x6)
APPG_IN_GGGA(x1, x2, x3, x4)  =  APPG_IN_GGGA(x1, x2, x3)
U17_GGGA(x1, x2, x3, x4, x5, x6)  =  U17_GGGA(x1, x2, x3, x4, x6)
U35_GA(x1, x2, x3)  =  U35_GA(x1, x3)
U36_GA(x1, x2, x3, x4)  =  U36_GA(x1, x3, x4)
U37_GA(x1, x2, x3)  =  U37_GA(x1, x3)
U26_GA(x1, x2, x3, x4, x5, x6)  =  U26_GA(x1, x2, x3, x5, x6)
U27_GA(x1, x2, x3, x4, x5)  =  U27_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QSD_IN_GA(.(X1, .(X2, X3)), X4) → U21_GA(X1, X2, X3, X4, gtA_in_gg(X1, X2))
QSD_IN_GA(.(X1, .(X2, X3)), X4) → GTA_IN_GG(X1, X2)
GTA_IN_GG(s(X1), s(X2)) → U1_GG(X1, X2, gtA_in_gg(X1, X2))
GTA_IN_GG(s(X1), s(X2)) → GTA_IN_GG(X1, X2)
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U22_GA(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U23_GA(X1, X2, X3, X4, partB_in_ggaa(X1, X3, X5, X6))
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X5, X6)
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U2_GGAA(X1, X2, X3, X4, X5, gtA_in_gg(X1, X2))
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → GTA_IN_GG(X1, X2)
PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U4_GGAA(X1, X2, X3, X4, X5, partB_in_ggaa(X1, X3, X4, X5))
U3_GGAA(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → U5_GGAA(X1, X2, X3, X4, X5, leC_in_gg(X1, X2))
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → LEC_IN_GG(X1, X2)
LEC_IN_GG(s(X1), s(X2)) → U8_GG(X1, X2, leC_in_gg(X1, X2))
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → U6_GGAA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U6_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U7_GGAA(X1, X2, X3, X4, X5, partB_in_ggaa(X1, X3, X4, X5))
U6_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U24_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U25_GA(X1, X2, X3, X4, qsD_in_ga(.(X2, X5), X7))
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSD_IN_GA(.(X2, X5), X7)
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U28_GA(X1, X2, X3, X4, leC_in_gg(X1, X2))
QSD_IN_GA(.(X1, .(X2, X3)), X4) → LEC_IN_GG(X1, X2)
QSD_IN_GA(.(X1, .(X2, X3)), X4) → U29_GA(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U29_GA(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U30_GA(X1, X2, X3, X4, partB_in_ggaa(X1, X3, X5, X6))
U29_GA(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X5, X6)
U29_GA(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U31_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U31_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U32_GA(X1, X2, X3, X4, qsF_in_ga(X5, X7))
U31_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSF_IN_GA(X5, X7)
QSF_IN_GA(.(X1, X2), X3) → U9_GA(X1, X2, X3, partB_in_ggaa(X1, X2, X4, X5))
QSF_IN_GA(.(X1, X2), X3) → PARTB_IN_GGAA(X1, X2, X4, X5)
QSF_IN_GA(.(X1, X2), X3) → U10_GA(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U11_GA(X1, X2, X3, qsF_in_ga(X4, X6))
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → QSF_IN_GA(X4, X6)
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U12_GA(X1, X2, X3, X5, qscF_in_ga(X4, X6))
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U13_GA(X1, X2, X3, qsF_in_ga(X5, X7))
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → QSF_IN_GA(X5, X7)
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U14_GA(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U14_GA(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U15_GA(X1, X2, X3, appI_in_ggga(X6, X1, X7, X3))
U14_GA(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → APPI_IN_GGGA(X6, X1, X7, X3)
APPI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U16_GGGA(X1, X2, X3, X4, X5, appI_in_ggga(X2, X3, X4, X5))
APPI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPI_IN_GGGA(X2, X3, X4, X5)
U31_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U33_GA(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U33_GA(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U34_GA(X1, X2, X3, X4, pE_in_gagga(.(X2, X6), X8, X7, X1, X4))
U33_GA(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → PE_IN_GAGGA(.(X2, X6), X8, X7, X1, X4)
PE_IN_GAGGA(X1, X2, X3, X4, X5) → U18_GAGGA(X1, X2, X3, X4, X5, qsF_in_ga(X1, X2))
PE_IN_GAGGA(X1, X2, X3, X4, X5) → QSF_IN_GA(X1, X2)
PE_IN_GAGGA(X1, X2, X3, X4, X5) → U19_GAGGA(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U19_GAGGA(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U20_GAGGA(X1, X2, X3, X4, X5, appG_in_ggga(X3, X4, X2, X5))
U19_GAGGA(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → APPG_IN_GGGA(X3, X4, X2, X5)
APPG_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U17_GGGA(X1, X2, X3, X4, X5, appG_in_ggga(X2, X3, X4, X5))
APPG_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPG_IN_GGGA(X2, X3, X4, X5)
QSD_IN_GA(.(X1, []), X2) → U35_GA(X1, X2, qscH_in_a(X3))
U35_GA(X1, X2, qscH_out_a(X3)) → U36_GA(X1, X2, X3, qscH_in_a(X4))
U36_GA(X1, X2, X3, qscH_out_a(X4)) → U37_GA(X1, X2, appG_in_ggga(X3, X1, X4, X2))
U36_GA(X1, X2, X3, qscH_out_a(X4)) → APPG_IN_GGGA(X3, X1, X4, X2)
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U26_GA(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
U26_GA(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U27_GA(X1, X2, X3, X4, pE_in_gagga(X6, X8, X7, X1, X4))
U26_GA(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → PE_IN_GAGGA(X6, X8, X7, X1, X4)

The TRS R consists of the following rules:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
qsD_in_ga(x1, x2)  =  qsD_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
gtA_in_gg(x1, x2)  =  gtA_in_gg(x1, x2)
s(x1)  =  s(x1)
gtcA_in_gg(x1, x2)  =  gtcA_in_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
0  =  0
gtcA_out_gg(x1, x2)  =  gtcA_out_gg(x1, x2)
partB_in_ggaa(x1, x2, x3, x4)  =  partB_in_ggaa(x1, x2)
leC_in_gg(x1, x2)  =  leC_in_gg(x1, x2)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U40_ggaa(x1, x2, x3, x4, x5, x6)  =  U40_ggaa(x1, x2, x3, x6)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qsF_in_ga(x1, x2)  =  qsF_in_ga(x1)
qscF_in_ga(x1, x2)  =  qscF_in_ga(x1)
U56_ga(x1, x2, x3, x4)  =  U56_ga(x1, x2, x4)
U57_ga(x1, x2, x3, x4, x5)  =  U57_ga(x1, x2, x4, x5)
qscF_out_ga(x1, x2)  =  qscF_out_ga(x1, x2)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4)  =  U59_ga(x1, x2, x4)
appcI_in_ggga(x1, x2, x3, x4)  =  appcI_in_ggga(x1, x2, x3)
U60_ggga(x1, x2, x3, x4, x5, x6)  =  U60_ggga(x1, x2, x3, x4, x6)
appcI_out_ggga(x1, x2, x3, x4)  =  appcI_out_ggga(x1, x2, x3, x4)
appI_in_ggga(x1, x2, x3, x4)  =  appI_in_ggga(x1, x2, x3)
pE_in_gagga(x1, x2, x3, x4, x5)  =  pE_in_gagga(x1, x3, x4)
appG_in_ggga(x1, x2, x3, x4)  =  appG_in_ggga(x1, x2, x3)
qscH_in_a(x1)  =  qscH_in_a
qscH_out_a(x1)  =  qscH_out_a(x1)
qscD_in_ga(x1, x2)  =  qscD_in_ga(x1)
U45_ga(x1, x2, x3, x4, x5)  =  U45_ga(x1, x2, x3, x5)
U46_ga(x1, x2, x3, x4, x5)  =  U46_ga(x1, x2, x3, x5)
U47_ga(x1, x2, x3, x4, x5, x6)  =  U47_ga(x1, x2, x3, x5, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
qcE_in_gagga(x1, x2, x3, x4, x5)  =  qcE_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
appcG_in_ggga(x1, x2, x3, x4)  =  appcG_in_ggga(x1, x2, x3)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
appcG_out_ggga(x1, x2, x3, x4)  =  appcG_out_ggga(x1, x2, x3, x4)
qcE_out_gagga(x1, x2, x3, x4, x5)  =  qcE_out_gagga(x1, x2, x3, x4, x5)
qscD_out_ga(x1, x2)  =  qscD_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
U54_ga(x1, x2, x3, x4)  =  U54_ga(x1, x3, x4)
U55_ga(x1, x2, x3)  =  U55_ga(x1, x3)
U48_ga(x1, x2, x3, x4, x5)  =  U48_ga(x1, x2, x3, x5)
QSD_IN_GA(x1, x2)  =  QSD_IN_GA(x1)
U21_GA(x1, x2, x3, x4, x5)  =  U21_GA(x1, x2, x3, x5)
GTA_IN_GG(x1, x2)  =  GTA_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x1, x2, x3)
U22_GA(x1, x2, x3, x4, x5)  =  U22_GA(x1, x2, x3, x5)
U23_GA(x1, x2, x3, x4, x5)  =  U23_GA(x1, x2, x3, x5)
PARTB_IN_GGAA(x1, x2, x3, x4)  =  PARTB_IN_GGAA(x1, x2)
U2_GGAA(x1, x2, x3, x4, x5, x6)  =  U2_GGAA(x1, x2, x3, x6)
U3_GGAA(x1, x2, x3, x4, x5, x6)  =  U3_GGAA(x1, x2, x3, x6)
U4_GGAA(x1, x2, x3, x4, x5, x6)  =  U4_GGAA(x1, x2, x3, x6)
U5_GGAA(x1, x2, x3, x4, x5, x6)  =  U5_GGAA(x1, x2, x3, x6)
LEC_IN_GG(x1, x2)  =  LEC_IN_GG(x1, x2)
U8_GG(x1, x2, x3)  =  U8_GG(x1, x2, x3)
U6_GGAA(x1, x2, x3, x4, x5, x6)  =  U6_GGAA(x1, x2, x3, x6)
U7_GGAA(x1, x2, x3, x4, x5, x6)  =  U7_GGAA(x1, x2, x3, x6)
U24_GA(x1, x2, x3, x4, x5)  =  U24_GA(x1, x2, x3, x5)
U25_GA(x1, x2, x3, x4, x5)  =  U25_GA(x1, x2, x3, x5)
U28_GA(x1, x2, x3, x4, x5)  =  U28_GA(x1, x2, x3, x5)
U29_GA(x1, x2, x3, x4, x5)  =  U29_GA(x1, x2, x3, x5)
U30_GA(x1, x2, x3, x4, x5)  =  U30_GA(x1, x2, x3, x5)
U31_GA(x1, x2, x3, x4, x5)  =  U31_GA(x1, x2, x3, x5)
U32_GA(x1, x2, x3, x4, x5)  =  U32_GA(x1, x2, x3, x5)
QSF_IN_GA(x1, x2)  =  QSF_IN_GA(x1)
U9_GA(x1, x2, x3, x4)  =  U9_GA(x1, x2, x4)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
U11_GA(x1, x2, x3, x4)  =  U11_GA(x1, x2, x4)
U12_GA(x1, x2, x3, x4, x5)  =  U12_GA(x1, x2, x4, x5)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x2, x4)
U14_GA(x1, x2, x3, x4, x5)  =  U14_GA(x1, x2, x4, x5)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x2, x4)
APPI_IN_GGGA(x1, x2, x3, x4)  =  APPI_IN_GGGA(x1, x2, x3)
U16_GGGA(x1, x2, x3, x4, x5, x6)  =  U16_GGGA(x1, x2, x3, x4, x6)
U33_GA(x1, x2, x3, x4, x5, x6)  =  U33_GA(x1, x2, x3, x5, x6)
U34_GA(x1, x2, x3, x4, x5)  =  U34_GA(x1, x2, x3, x5)
PE_IN_GAGGA(x1, x2, x3, x4, x5)  =  PE_IN_GAGGA(x1, x3, x4)
U18_GAGGA(x1, x2, x3, x4, x5, x6)  =  U18_GAGGA(x1, x3, x4, x6)
U19_GAGGA(x1, x2, x3, x4, x5, x6)  =  U19_GAGGA(x1, x3, x4, x6)
U20_GAGGA(x1, x2, x3, x4, x5, x6)  =  U20_GAGGA(x1, x3, x4, x6)
APPG_IN_GGGA(x1, x2, x3, x4)  =  APPG_IN_GGGA(x1, x2, x3)
U17_GGGA(x1, x2, x3, x4, x5, x6)  =  U17_GGGA(x1, x2, x3, x4, x6)
U35_GA(x1, x2, x3)  =  U35_GA(x1, x3)
U36_GA(x1, x2, x3, x4)  =  U36_GA(x1, x3, x4)
U37_GA(x1, x2, x3)  =  U37_GA(x1, x3)
U26_GA(x1, x2, x3, x4, x5, x6)  =  U26_GA(x1, x2, x3, x5, x6)
U27_GA(x1, x2, x3, x4, x5)  =  U27_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 7 SCCs with 45 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPG_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPG_IN_GGGA(X2, X3, X4, X5)

The TRS R consists of the following rules:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
gtcA_in_gg(x1, x2)  =  gtcA_in_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
0  =  0
gtcA_out_gg(x1, x2)  =  gtcA_out_gg(x1, x2)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U40_ggaa(x1, x2, x3, x4, x5, x6)  =  U40_ggaa(x1, x2, x3, x6)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscF_in_ga(x1, x2)  =  qscF_in_ga(x1)
U56_ga(x1, x2, x3, x4)  =  U56_ga(x1, x2, x4)
U57_ga(x1, x2, x3, x4, x5)  =  U57_ga(x1, x2, x4, x5)
qscF_out_ga(x1, x2)  =  qscF_out_ga(x1, x2)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4)  =  U59_ga(x1, x2, x4)
appcI_in_ggga(x1, x2, x3, x4)  =  appcI_in_ggga(x1, x2, x3)
U60_ggga(x1, x2, x3, x4, x5, x6)  =  U60_ggga(x1, x2, x3, x4, x6)
appcI_out_ggga(x1, x2, x3, x4)  =  appcI_out_ggga(x1, x2, x3, x4)
qscH_in_a(x1)  =  qscH_in_a
qscH_out_a(x1)  =  qscH_out_a(x1)
qscD_in_ga(x1, x2)  =  qscD_in_ga(x1)
U45_ga(x1, x2, x3, x4, x5)  =  U45_ga(x1, x2, x3, x5)
U46_ga(x1, x2, x3, x4, x5)  =  U46_ga(x1, x2, x3, x5)
U47_ga(x1, x2, x3, x4, x5, x6)  =  U47_ga(x1, x2, x3, x5, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
qcE_in_gagga(x1, x2, x3, x4, x5)  =  qcE_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
appcG_in_ggga(x1, x2, x3, x4)  =  appcG_in_ggga(x1, x2, x3)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
appcG_out_ggga(x1, x2, x3, x4)  =  appcG_out_ggga(x1, x2, x3, x4)
qcE_out_gagga(x1, x2, x3, x4, x5)  =  qcE_out_gagga(x1, x2, x3, x4, x5)
qscD_out_ga(x1, x2)  =  qscD_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
U54_ga(x1, x2, x3, x4)  =  U54_ga(x1, x3, x4)
U55_ga(x1, x2, x3)  =  U55_ga(x1, x3)
U48_ga(x1, x2, x3, x4, x5)  =  U48_ga(x1, x2, x3, x5)
APPG_IN_GGGA(x1, x2, x3, x4)  =  APPG_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPG_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPG_IN_GGGA(X2, X3, X4, X5)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPG_IN_GGGA(x1, x2, x3, x4)  =  APPG_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPG_IN_GGGA(.(X1, X2), X3, X4) → APPG_IN_GGGA(X2, X3, X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPG_IN_GGGA(.(X1, X2), X3, X4) → APPG_IN_GGGA(X2, X3, X4)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPI_IN_GGGA(X2, X3, X4, X5)

The TRS R consists of the following rules:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
gtcA_in_gg(x1, x2)  =  gtcA_in_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
0  =  0
gtcA_out_gg(x1, x2)  =  gtcA_out_gg(x1, x2)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U40_ggaa(x1, x2, x3, x4, x5, x6)  =  U40_ggaa(x1, x2, x3, x6)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscF_in_ga(x1, x2)  =  qscF_in_ga(x1)
U56_ga(x1, x2, x3, x4)  =  U56_ga(x1, x2, x4)
U57_ga(x1, x2, x3, x4, x5)  =  U57_ga(x1, x2, x4, x5)
qscF_out_ga(x1, x2)  =  qscF_out_ga(x1, x2)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4)  =  U59_ga(x1, x2, x4)
appcI_in_ggga(x1, x2, x3, x4)  =  appcI_in_ggga(x1, x2, x3)
U60_ggga(x1, x2, x3, x4, x5, x6)  =  U60_ggga(x1, x2, x3, x4, x6)
appcI_out_ggga(x1, x2, x3, x4)  =  appcI_out_ggga(x1, x2, x3, x4)
qscH_in_a(x1)  =  qscH_in_a
qscH_out_a(x1)  =  qscH_out_a(x1)
qscD_in_ga(x1, x2)  =  qscD_in_ga(x1)
U45_ga(x1, x2, x3, x4, x5)  =  U45_ga(x1, x2, x3, x5)
U46_ga(x1, x2, x3, x4, x5)  =  U46_ga(x1, x2, x3, x5)
U47_ga(x1, x2, x3, x4, x5, x6)  =  U47_ga(x1, x2, x3, x5, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
qcE_in_gagga(x1, x2, x3, x4, x5)  =  qcE_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
appcG_in_ggga(x1, x2, x3, x4)  =  appcG_in_ggga(x1, x2, x3)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
appcG_out_ggga(x1, x2, x3, x4)  =  appcG_out_ggga(x1, x2, x3, x4)
qcE_out_gagga(x1, x2, x3, x4, x5)  =  qcE_out_gagga(x1, x2, x3, x4, x5)
qscD_out_ga(x1, x2)  =  qscD_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
U54_ga(x1, x2, x3, x4)  =  U54_ga(x1, x3, x4)
U55_ga(x1, x2, x3)  =  U55_ga(x1, x3)
U48_ga(x1, x2, x3, x4, x5)  =  U48_ga(x1, x2, x3, x5)
APPI_IN_GGGA(x1, x2, x3, x4)  =  APPI_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPI_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPI_IN_GGGA(X2, X3, X4, X5)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPI_IN_GGGA(x1, x2, x3, x4)  =  APPI_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPI_IN_GGGA(.(X1, X2), X3, X4) → APPI_IN_GGGA(X2, X3, X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPI_IN_GGGA(.(X1, X2), X3, X4) → APPI_IN_GGGA(X2, X3, X4)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)

The TRS R consists of the following rules:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
gtcA_in_gg(x1, x2)  =  gtcA_in_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
0  =  0
gtcA_out_gg(x1, x2)  =  gtcA_out_gg(x1, x2)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U40_ggaa(x1, x2, x3, x4, x5, x6)  =  U40_ggaa(x1, x2, x3, x6)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscF_in_ga(x1, x2)  =  qscF_in_ga(x1)
U56_ga(x1, x2, x3, x4)  =  U56_ga(x1, x2, x4)
U57_ga(x1, x2, x3, x4, x5)  =  U57_ga(x1, x2, x4, x5)
qscF_out_ga(x1, x2)  =  qscF_out_ga(x1, x2)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4)  =  U59_ga(x1, x2, x4)
appcI_in_ggga(x1, x2, x3, x4)  =  appcI_in_ggga(x1, x2, x3)
U60_ggga(x1, x2, x3, x4, x5, x6)  =  U60_ggga(x1, x2, x3, x4, x6)
appcI_out_ggga(x1, x2, x3, x4)  =  appcI_out_ggga(x1, x2, x3, x4)
qscH_in_a(x1)  =  qscH_in_a
qscH_out_a(x1)  =  qscH_out_a(x1)
qscD_in_ga(x1, x2)  =  qscD_in_ga(x1)
U45_ga(x1, x2, x3, x4, x5)  =  U45_ga(x1, x2, x3, x5)
U46_ga(x1, x2, x3, x4, x5)  =  U46_ga(x1, x2, x3, x5)
U47_ga(x1, x2, x3, x4, x5, x6)  =  U47_ga(x1, x2, x3, x5, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
qcE_in_gagga(x1, x2, x3, x4, x5)  =  qcE_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
appcG_in_ggga(x1, x2, x3, x4)  =  appcG_in_ggga(x1, x2, x3)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
appcG_out_ggga(x1, x2, x3, x4)  =  appcG_out_ggga(x1, x2, x3, x4)
qcE_out_gagga(x1, x2, x3, x4, x5)  =  qcE_out_gagga(x1, x2, x3, x4, x5)
qscD_out_ga(x1, x2)  =  qscD_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
U54_ga(x1, x2, x3, x4)  =  U54_ga(x1, x3, x4)
U55_ga(x1, x2, x3)  =  U55_ga(x1, x3)
U48_ga(x1, x2, x3, x4, x5)  =  U48_ga(x1, x2, x3, x5)
LEC_IN_GG(x1, x2)  =  LEC_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(29) YES

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GTA_IN_GG(s(X1), s(X2)) → GTA_IN_GG(X1, X2)

The TRS R consists of the following rules:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
gtcA_in_gg(x1, x2)  =  gtcA_in_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
0  =  0
gtcA_out_gg(x1, x2)  =  gtcA_out_gg(x1, x2)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U40_ggaa(x1, x2, x3, x4, x5, x6)  =  U40_ggaa(x1, x2, x3, x6)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscF_in_ga(x1, x2)  =  qscF_in_ga(x1)
U56_ga(x1, x2, x3, x4)  =  U56_ga(x1, x2, x4)
U57_ga(x1, x2, x3, x4, x5)  =  U57_ga(x1, x2, x4, x5)
qscF_out_ga(x1, x2)  =  qscF_out_ga(x1, x2)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4)  =  U59_ga(x1, x2, x4)
appcI_in_ggga(x1, x2, x3, x4)  =  appcI_in_ggga(x1, x2, x3)
U60_ggga(x1, x2, x3, x4, x5, x6)  =  U60_ggga(x1, x2, x3, x4, x6)
appcI_out_ggga(x1, x2, x3, x4)  =  appcI_out_ggga(x1, x2, x3, x4)
qscH_in_a(x1)  =  qscH_in_a
qscH_out_a(x1)  =  qscH_out_a(x1)
qscD_in_ga(x1, x2)  =  qscD_in_ga(x1)
U45_ga(x1, x2, x3, x4, x5)  =  U45_ga(x1, x2, x3, x5)
U46_ga(x1, x2, x3, x4, x5)  =  U46_ga(x1, x2, x3, x5)
U47_ga(x1, x2, x3, x4, x5, x6)  =  U47_ga(x1, x2, x3, x5, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
qcE_in_gagga(x1, x2, x3, x4, x5)  =  qcE_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
appcG_in_ggga(x1, x2, x3, x4)  =  appcG_in_ggga(x1, x2, x3)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
appcG_out_ggga(x1, x2, x3, x4)  =  appcG_out_ggga(x1, x2, x3, x4)
qcE_out_gagga(x1, x2, x3, x4, x5)  =  qcE_out_gagga(x1, x2, x3, x4, x5)
qscD_out_ga(x1, x2)  =  qscD_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
U54_ga(x1, x2, x3, x4)  =  U54_ga(x1, x3, x4)
U55_ga(x1, x2, x3)  =  U55_ga(x1, x3)
U48_ga(x1, x2, x3, x4, x5)  =  U48_ga(x1, x2, x3, x5)
GTA_IN_GG(x1, x2)  =  GTA_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(31) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GTA_IN_GG(s(X1), s(X2)) → GTA_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GTA_IN_GG(s(X1), s(X2)) → GTA_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • GTA_IN_GG(s(X1), s(X2)) → GTA_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(36) YES

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → U6_GGAA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U6_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)

The TRS R consists of the following rules:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
gtcA_in_gg(x1, x2)  =  gtcA_in_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
0  =  0
gtcA_out_gg(x1, x2)  =  gtcA_out_gg(x1, x2)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U40_ggaa(x1, x2, x3, x4, x5, x6)  =  U40_ggaa(x1, x2, x3, x6)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscF_in_ga(x1, x2)  =  qscF_in_ga(x1)
U56_ga(x1, x2, x3, x4)  =  U56_ga(x1, x2, x4)
U57_ga(x1, x2, x3, x4, x5)  =  U57_ga(x1, x2, x4, x5)
qscF_out_ga(x1, x2)  =  qscF_out_ga(x1, x2)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4)  =  U59_ga(x1, x2, x4)
appcI_in_ggga(x1, x2, x3, x4)  =  appcI_in_ggga(x1, x2, x3)
U60_ggga(x1, x2, x3, x4, x5, x6)  =  U60_ggga(x1, x2, x3, x4, x6)
appcI_out_ggga(x1, x2, x3, x4)  =  appcI_out_ggga(x1, x2, x3, x4)
qscH_in_a(x1)  =  qscH_in_a
qscH_out_a(x1)  =  qscH_out_a(x1)
qscD_in_ga(x1, x2)  =  qscD_in_ga(x1)
U45_ga(x1, x2, x3, x4, x5)  =  U45_ga(x1, x2, x3, x5)
U46_ga(x1, x2, x3, x4, x5)  =  U46_ga(x1, x2, x3, x5)
U47_ga(x1, x2, x3, x4, x5, x6)  =  U47_ga(x1, x2, x3, x5, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
qcE_in_gagga(x1, x2, x3, x4, x5)  =  qcE_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
appcG_in_ggga(x1, x2, x3, x4)  =  appcG_in_ggga(x1, x2, x3)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
appcG_out_ggga(x1, x2, x3, x4)  =  appcG_out_ggga(x1, x2, x3, x4)
qcE_out_gagga(x1, x2, x3, x4, x5)  =  qcE_out_gagga(x1, x2, x3, x4, x5)
qscD_out_ga(x1, x2)  =  qscD_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
U54_ga(x1, x2, x3, x4)  =  U54_ga(x1, x3, x4)
U55_ga(x1, x2, x3)  =  U55_ga(x1, x3)
U48_ga(x1, x2, x3, x4, x5)  =  U48_ga(x1, x2, x3, x5)
PARTB_IN_GGAA(x1, x2, x3, x4)  =  PARTB_IN_GGAA(x1, x2)
U3_GGAA(x1, x2, x3, x4, x5, x6)  =  U3_GGAA(x1, x2, x3, x6)
U6_GGAA(x1, x2, x3, x4, x5, x6)  =  U6_GGAA(x1, x2, x3, x6)

We have to consider all (P,R,Pi)-chains

(38) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(39) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PARTB_IN_GGAA(X1, .(X2, X3), .(X2, X4), X5) → U3_GGAA(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)
PARTB_IN_GGAA(X1, .(X2, X3), X4, .(X2, X5)) → U6_GGAA(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U6_GGAA(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3, X4, X5)

The TRS R consists of the following rules:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
gtcA_in_gg(x1, x2)  =  gtcA_in_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
0  =  0
gtcA_out_gg(x1, x2)  =  gtcA_out_gg(x1, x2)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
PARTB_IN_GGAA(x1, x2, x3, x4)  =  PARTB_IN_GGAA(x1, x2)
U3_GGAA(x1, x2, x3, x4, x5, x6)  =  U3_GGAA(x1, x2, x3, x6)
U6_GGAA(x1, x2, x3, x4, x5, x6)  =  U6_GGAA(x1, x2, x3, x6)

We have to consider all (P,R,Pi)-chains

(40) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PARTB_IN_GGAA(X1, .(X2, X3)) → U3_GGAA(X1, X2, X3, gtcA_in_gg(X1, X2))
U3_GGAA(X1, X2, X3, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3)
PARTB_IN_GGAA(X1, .(X2, X3)) → U6_GGAA(X1, X2, X3, lecC_in_gg(X1, X2))
U6_GGAA(X1, X2, X3, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3)

The TRS R consists of the following rules:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

gtcA_in_gg(x0, x1)
lecC_in_gg(x0, x1)
U39_gg(x0, x1, x2)
U44_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(42) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U3_GGAA(X1, X2, X3, gtcA_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3)
    The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2

  • U6_GGAA(X1, X2, X3, lecC_out_gg(X1, X2)) → PARTB_IN_GGAA(X1, X3)
    The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2

  • PARTB_IN_GGAA(X1, .(X2, X3)) → U3_GGAA(X1, X2, X3, gtcA_in_gg(X1, X2))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

  • PARTB_IN_GGAA(X1, .(X2, X3)) → U6_GGAA(X1, X2, X3, lecC_in_gg(X1, X2))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(43) YES

(44) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QSF_IN_GA(.(X1, X2), X3) → U10_GA(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → QSF_IN_GA(X4, X6)
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U12_GA(X1, X2, X3, X5, qscF_in_ga(X4, X6))
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → QSF_IN_GA(X5, X7)

The TRS R consists of the following rules:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
gtcA_in_gg(x1, x2)  =  gtcA_in_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
0  =  0
gtcA_out_gg(x1, x2)  =  gtcA_out_gg(x1, x2)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U40_ggaa(x1, x2, x3, x4, x5, x6)  =  U40_ggaa(x1, x2, x3, x6)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscF_in_ga(x1, x2)  =  qscF_in_ga(x1)
U56_ga(x1, x2, x3, x4)  =  U56_ga(x1, x2, x4)
U57_ga(x1, x2, x3, x4, x5)  =  U57_ga(x1, x2, x4, x5)
qscF_out_ga(x1, x2)  =  qscF_out_ga(x1, x2)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4)  =  U59_ga(x1, x2, x4)
appcI_in_ggga(x1, x2, x3, x4)  =  appcI_in_ggga(x1, x2, x3)
U60_ggga(x1, x2, x3, x4, x5, x6)  =  U60_ggga(x1, x2, x3, x4, x6)
appcI_out_ggga(x1, x2, x3, x4)  =  appcI_out_ggga(x1, x2, x3, x4)
qscH_in_a(x1)  =  qscH_in_a
qscH_out_a(x1)  =  qscH_out_a(x1)
qscD_in_ga(x1, x2)  =  qscD_in_ga(x1)
U45_ga(x1, x2, x3, x4, x5)  =  U45_ga(x1, x2, x3, x5)
U46_ga(x1, x2, x3, x4, x5)  =  U46_ga(x1, x2, x3, x5)
U47_ga(x1, x2, x3, x4, x5, x6)  =  U47_ga(x1, x2, x3, x5, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
qcE_in_gagga(x1, x2, x3, x4, x5)  =  qcE_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
appcG_in_ggga(x1, x2, x3, x4)  =  appcG_in_ggga(x1, x2, x3)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
appcG_out_ggga(x1, x2, x3, x4)  =  appcG_out_ggga(x1, x2, x3, x4)
qcE_out_gagga(x1, x2, x3, x4, x5)  =  qcE_out_gagga(x1, x2, x3, x4, x5)
qscD_out_ga(x1, x2)  =  qscD_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
U54_ga(x1, x2, x3, x4)  =  U54_ga(x1, x3, x4)
U55_ga(x1, x2, x3)  =  U55_ga(x1, x3)
U48_ga(x1, x2, x3, x4, x5)  =  U48_ga(x1, x2, x3, x5)
QSF_IN_GA(x1, x2)  =  QSF_IN_GA(x1)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
U12_GA(x1, x2, x3, x4, x5)  =  U12_GA(x1, x2, x4, x5)

We have to consider all (P,R,Pi)-chains

(45) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(46) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QSF_IN_GA(.(X1, X2), X3) → U10_GA(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → QSF_IN_GA(X4, X6)
U10_GA(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U12_GA(X1, X2, X3, X5, qscF_in_ga(X4, X6))
U12_GA(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → QSF_IN_GA(X5, X7)

The TRS R consists of the following rules:

partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
qscF_in_ga([], []) → qscF_out_ga([], [])
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
gtcA_in_gg(x1, x2)  =  gtcA_in_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
0  =  0
gtcA_out_gg(x1, x2)  =  gtcA_out_gg(x1, x2)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U40_ggaa(x1, x2, x3, x4, x5, x6)  =  U40_ggaa(x1, x2, x3, x6)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscF_in_ga(x1, x2)  =  qscF_in_ga(x1)
U56_ga(x1, x2, x3, x4)  =  U56_ga(x1, x2, x4)
U57_ga(x1, x2, x3, x4, x5)  =  U57_ga(x1, x2, x4, x5)
qscF_out_ga(x1, x2)  =  qscF_out_ga(x1, x2)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4)  =  U59_ga(x1, x2, x4)
appcI_in_ggga(x1, x2, x3, x4)  =  appcI_in_ggga(x1, x2, x3)
U60_ggga(x1, x2, x3, x4, x5, x6)  =  U60_ggga(x1, x2, x3, x4, x6)
appcI_out_ggga(x1, x2, x3, x4)  =  appcI_out_ggga(x1, x2, x3, x4)
QSF_IN_GA(x1, x2)  =  QSF_IN_GA(x1)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
U12_GA(x1, x2, x3, x4, x5)  =  U12_GA(x1, x2, x4, x5)

We have to consider all (P,R,Pi)-chains

(47) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QSF_IN_GA(.(X1, X2)) → U10_GA(X1, X2, partcB_in_ggaa(X1, X2))
U10_GA(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → QSF_IN_GA(X4)
U10_GA(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → U12_GA(X1, X2, X5, qscF_in_ga(X4))
U12_GA(X1, X2, X5, qscF_out_ga(X4, X6)) → QSF_IN_GA(X5)

The TRS R consists of the following rules:

partcB_in_ggaa(X1, .(X2, X3)) → U40_ggaa(X1, X2, X3, gtcA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U42_ggaa(X1, X2, X3, lecC_in_gg(X1, X2))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
qscF_in_ga(.(X1, X2)) → U56_ga(X1, X2, partcB_in_ggaa(X1, X2))
qscF_in_ga([]) → qscF_out_ga([], [])
U40_ggaa(X1, X2, X3, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U42_ggaa(X1, X2, X3, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U56_ga(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X5, qscF_in_ga(X4))
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U41_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U43_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U57_ga(X1, X2, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X6, qscF_in_ga(X5))
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U58_ga(X1, X2, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, appcI_in_ggga(X6, X1, X7))
U59_ga(X1, X2, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
appcI_in_ggga(.(X1, X2), X3, X4) → U60_ggga(X1, X2, X3, X4, appcI_in_ggga(X2, X3, X4))
appcI_in_ggga([], X1, X2) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))

The set Q consists of the following terms:

partcB_in_ggaa(x0, x1)
qscF_in_ga(x0)
U40_ggaa(x0, x1, x2, x3)
U42_ggaa(x0, x1, x2, x3)
U56_ga(x0, x1, x2)
gtcA_in_gg(x0, x1)
U41_ggaa(x0, x1, x2, x3)
lecC_in_gg(x0, x1)
U43_ggaa(x0, x1, x2, x3)
U57_ga(x0, x1, x2, x3)
U39_gg(x0, x1, x2)
U44_gg(x0, x1, x2)
U58_ga(x0, x1, x2, x3)
U59_ga(x0, x1, x2)
appcI_in_ggga(x0, x1, x2)
U60_ggga(x0, x1, x2, x3, x4)

We have to consider all (P,Q,R)-chains.

(49) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


QSF_IN_GA(.(X1, X2)) → U10_GA(X1, X2, partcB_in_ggaa(X1, X2))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x2   
POL(0) = 0   
POL(QSF_IN_GA(x1)) = x1   
POL(U10_GA(x1, x2, x3)) = x3   
POL(U12_GA(x1, x2, x3, x4)) = x3   
POL(U39_gg(x1, x2, x3)) = 0   
POL(U40_ggaa(x1, x2, x3, x4)) = 1 + x3   
POL(U41_ggaa(x1, x2, x3, x4)) = 1 + x4   
POL(U42_ggaa(x1, x2, x3, x4)) = 1 + x3   
POL(U43_ggaa(x1, x2, x3, x4)) = 1 + x4   
POL(U44_gg(x1, x2, x3)) = 0   
POL(U56_ga(x1, x2, x3)) = 0   
POL(U57_ga(x1, x2, x3, x4)) = 0   
POL(U58_ga(x1, x2, x3, x4)) = 0   
POL(U59_ga(x1, x2, x3)) = 0   
POL(U60_ggga(x1, x2, x3, x4, x5)) = 0   
POL([]) = 0   
POL(appcI_in_ggga(x1, x2, x3)) = 0   
POL(appcI_out_ggga(x1, x2, x3, x4)) = 0   
POL(gtcA_in_gg(x1, x2)) = 0   
POL(gtcA_out_gg(x1, x2)) = 0   
POL(lecC_in_gg(x1, x2)) = 0   
POL(lecC_out_gg(x1, x2)) = 0   
POL(partcB_in_ggaa(x1, x2)) = x2   
POL(partcB_out_ggaa(x1, x2, x3, x4)) = x3 + x4   
POL(qscF_in_ga(x1)) = 0   
POL(qscF_out_ga(x1, x2)) = 0   
POL(s(x1)) = 0   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

partcB_in_ggaa(X1, .(X2, X3)) → U40_ggaa(X1, X2, X3, gtcA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U42_ggaa(X1, X2, X3, lecC_in_gg(X1, X2))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
U40_ggaa(X1, X2, X3, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U41_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
U42_ggaa(X1, X2, X3, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U43_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))

(50) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U10_GA(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → QSF_IN_GA(X4)
U10_GA(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → U12_GA(X1, X2, X5, qscF_in_ga(X4))
U12_GA(X1, X2, X5, qscF_out_ga(X4, X6)) → QSF_IN_GA(X5)

The TRS R consists of the following rules:

partcB_in_ggaa(X1, .(X2, X3)) → U40_ggaa(X1, X2, X3, gtcA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U42_ggaa(X1, X2, X3, lecC_in_gg(X1, X2))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
qscF_in_ga(.(X1, X2)) → U56_ga(X1, X2, partcB_in_ggaa(X1, X2))
qscF_in_ga([]) → qscF_out_ga([], [])
U40_ggaa(X1, X2, X3, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U42_ggaa(X1, X2, X3, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U56_ga(X1, X2, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X5, qscF_in_ga(X4))
gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U41_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U43_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U57_ga(X1, X2, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X6, qscF_in_ga(X5))
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U58_ga(X1, X2, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, appcI_in_ggga(X6, X1, X7))
U59_ga(X1, X2, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
appcI_in_ggga(.(X1, X2), X3, X4) → U60_ggga(X1, X2, X3, X4, appcI_in_ggga(X2, X3, X4))
appcI_in_ggga([], X1, X2) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))

The set Q consists of the following terms:

partcB_in_ggaa(x0, x1)
qscF_in_ga(x0)
U40_ggaa(x0, x1, x2, x3)
U42_ggaa(x0, x1, x2, x3)
U56_ga(x0, x1, x2)
gtcA_in_gg(x0, x1)
U41_ggaa(x0, x1, x2, x3)
lecC_in_gg(x0, x1)
U43_ggaa(x0, x1, x2, x3)
U57_ga(x0, x1, x2, x3)
U39_gg(x0, x1, x2)
U44_gg(x0, x1, x2)
U58_ga(x0, x1, x2, x3)
U59_ga(x0, x1, x2)
appcI_in_ggga(x0, x1, x2)
U60_ggga(x0, x1, x2, x3, x4)

We have to consider all (P,Q,R)-chains.

(51) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(52) TRUE

(53) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QSD_IN_GA(.(X1, .(X2, X3)), X4) → U22_GA(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U24_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSD_IN_GA(.(X2, X5), X7)

The TRS R consists of the following rules:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
qscF_in_ga(.(X1, X2), X3) → U56_ga(X1, X2, X3, partcB_in_ggaa(X1, X2, X4, X5))
U56_ga(X1, X2, X3, partcB_out_ggaa(X1, X2, X4, X5)) → U57_ga(X1, X2, X3, X5, qscF_in_ga(X4, X6))
qscF_in_ga([], []) → qscF_out_ga([], [])
U57_ga(X1, X2, X3, X5, qscF_out_ga(X4, X6)) → U58_ga(X1, X2, X3, X6, qscF_in_ga(X5, X7))
U58_ga(X1, X2, X3, X6, qscF_out_ga(X5, X7)) → U59_ga(X1, X2, X3, appcI_in_ggga(X6, X1, X7, X3))
appcI_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U60_ggga(X1, X2, X3, X4, X5, appcI_in_ggga(X2, X3, X4, X5))
appcI_in_ggga([], X1, X2, .(X1, X2)) → appcI_out_ggga([], X1, X2, .(X1, X2))
U60_ggga(X1, X2, X3, X4, X5, appcI_out_ggga(X2, X3, X4, X5)) → appcI_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U59_ga(X1, X2, X3, appcI_out_ggga(X6, X1, X7, X3)) → qscF_out_ga(.(X1, X2), X3)
qscH_in_a([]) → qscH_out_a([])
qscD_in_ga(.(X1, .(X2, X3)), X4) → U45_ga(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U45_ga(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U46_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U46_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U47_ga(X1, X2, X3, X4, X6, qscD_in_ga(.(X2, X5), X7))
qscD_in_ga(.(X1, .(X2, X3)), X4) → U49_ga(X1, X2, X3, X4, lecC_in_gg(X1, X2))
U49_ga(X1, X2, X3, X4, lecC_out_gg(X1, X2)) → U50_ga(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U50_ga(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → U51_ga(X1, X2, X3, X4, X6, qscF_in_ga(X5, X7))
U51_ga(X1, X2, X3, X4, X6, qscF_out_ga(X5, X7)) → U52_ga(X1, X2, X3, X4, qcE_in_gagga(.(X2, X6), X8, X7, X1, X4))
qcE_in_gagga(X1, X2, X3, X4, X5) → U62_gagga(X1, X2, X3, X4, X5, qscF_in_ga(X1, X2))
U62_gagga(X1, X2, X3, X4, X5, qscF_out_ga(X1, X2)) → U63_gagga(X1, X2, X3, X4, X5, appcG_in_ggga(X3, X4, X2, X5))
appcG_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U61_ggga(X1, X2, X3, X4, X5, appcG_in_ggga(X2, X3, X4, X5))
appcG_in_ggga([], X1, X2, .(X1, X2)) → appcG_out_ggga([], X1, X2, .(X1, X2))
U61_ggga(X1, X2, X3, X4, X5, appcG_out_ggga(X2, X3, X4, X5)) → appcG_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U63_gagga(X1, X2, X3, X4, X5, appcG_out_ggga(X3, X4, X2, X5)) → qcE_out_gagga(X1, X2, X3, X4, X5)
U52_ga(X1, X2, X3, X4, qcE_out_gagga(.(X2, X6), X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)
qscD_in_ga(.(X1, []), X2) → U53_ga(X1, X2, qscH_in_a(X3))
U53_ga(X1, X2, qscH_out_a(X3)) → U54_ga(X1, X2, X3, qscH_in_a(X4))
U54_ga(X1, X2, X3, qscH_out_a(X4)) → U55_ga(X1, X2, appcG_in_ggga(X3, X1, X4, X2))
U55_ga(X1, X2, appcG_out_ggga(X3, X1, X4, X2)) → qscD_out_ga(.(X1, []), X2)
qscD_in_ga([], []) → qscD_out_ga([], [])
U47_ga(X1, X2, X3, X4, X6, qscD_out_ga(.(X2, X5), X7)) → U48_ga(X1, X2, X3, X4, qcE_in_gagga(X6, X8, X7, X1, X4))
U48_ga(X1, X2, X3, X4, qcE_out_gagga(X6, X8, X7, X1, X4)) → qscD_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
gtcA_in_gg(x1, x2)  =  gtcA_in_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
0  =  0
gtcA_out_gg(x1, x2)  =  gtcA_out_gg(x1, x2)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U40_ggaa(x1, x2, x3, x4, x5, x6)  =  U40_ggaa(x1, x2, x3, x6)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
qscF_in_ga(x1, x2)  =  qscF_in_ga(x1)
U56_ga(x1, x2, x3, x4)  =  U56_ga(x1, x2, x4)
U57_ga(x1, x2, x3, x4, x5)  =  U57_ga(x1, x2, x4, x5)
qscF_out_ga(x1, x2)  =  qscF_out_ga(x1, x2)
U58_ga(x1, x2, x3, x4, x5)  =  U58_ga(x1, x2, x4, x5)
U59_ga(x1, x2, x3, x4)  =  U59_ga(x1, x2, x4)
appcI_in_ggga(x1, x2, x3, x4)  =  appcI_in_ggga(x1, x2, x3)
U60_ggga(x1, x2, x3, x4, x5, x6)  =  U60_ggga(x1, x2, x3, x4, x6)
appcI_out_ggga(x1, x2, x3, x4)  =  appcI_out_ggga(x1, x2, x3, x4)
qscH_in_a(x1)  =  qscH_in_a
qscH_out_a(x1)  =  qscH_out_a(x1)
qscD_in_ga(x1, x2)  =  qscD_in_ga(x1)
U45_ga(x1, x2, x3, x4, x5)  =  U45_ga(x1, x2, x3, x5)
U46_ga(x1, x2, x3, x4, x5)  =  U46_ga(x1, x2, x3, x5)
U47_ga(x1, x2, x3, x4, x5, x6)  =  U47_ga(x1, x2, x3, x5, x6)
U49_ga(x1, x2, x3, x4, x5)  =  U49_ga(x1, x2, x3, x5)
U50_ga(x1, x2, x3, x4, x5)  =  U50_ga(x1, x2, x3, x5)
U51_ga(x1, x2, x3, x4, x5, x6)  =  U51_ga(x1, x2, x3, x5, x6)
U52_ga(x1, x2, x3, x4, x5)  =  U52_ga(x1, x2, x3, x5)
qcE_in_gagga(x1, x2, x3, x4, x5)  =  qcE_in_gagga(x1, x3, x4)
U62_gagga(x1, x2, x3, x4, x5, x6)  =  U62_gagga(x1, x3, x4, x6)
U63_gagga(x1, x2, x3, x4, x5, x6)  =  U63_gagga(x1, x2, x3, x4, x6)
appcG_in_ggga(x1, x2, x3, x4)  =  appcG_in_ggga(x1, x2, x3)
U61_ggga(x1, x2, x3, x4, x5, x6)  =  U61_ggga(x1, x2, x3, x4, x6)
appcG_out_ggga(x1, x2, x3, x4)  =  appcG_out_ggga(x1, x2, x3, x4)
qcE_out_gagga(x1, x2, x3, x4, x5)  =  qcE_out_gagga(x1, x2, x3, x4, x5)
qscD_out_ga(x1, x2)  =  qscD_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
U54_ga(x1, x2, x3, x4)  =  U54_ga(x1, x3, x4)
U55_ga(x1, x2, x3)  =  U55_ga(x1, x3)
U48_ga(x1, x2, x3, x4, x5)  =  U48_ga(x1, x2, x3, x5)
QSD_IN_GA(x1, x2)  =  QSD_IN_GA(x1)
U22_GA(x1, x2, x3, x4, x5)  =  U22_GA(x1, x2, x3, x5)
U24_GA(x1, x2, x3, x4, x5)  =  U24_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(54) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(55) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QSD_IN_GA(.(X1, .(X2, X3)), X4) → U22_GA(X1, X2, X3, X4, gtcA_in_gg(X1, X2))
U22_GA(X1, X2, X3, X4, gtcA_out_gg(X1, X2)) → U24_GA(X1, X2, X3, X4, partcB_in_ggaa(X1, X3, X5, X6))
U24_GA(X1, X2, X3, X4, partcB_out_ggaa(X1, X3, X5, X6)) → QSD_IN_GA(.(X2, X5), X7)

The TRS R consists of the following rules:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
partcB_in_ggaa(X1, .(X2, X3), .(X2, X4), X5) → U40_ggaa(X1, X2, X3, X4, X5, gtcA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3), X4, .(X2, X5)) → U42_ggaa(X1, X2, X3, X4, X5, lecC_in_gg(X1, X2))
partcB_in_ggaa(X1, [], [], []) → partcB_out_ggaa(X1, [], [], [])
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U40_ggaa(X1, X2, X3, X4, X5, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
U42_ggaa(X1, X2, X3, X4, X5, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, X4, X5, partcB_in_ggaa(X1, X3, X4, X5))
U41_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U43_ggaa(X1, X2, X3, X4, X5, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
gtcA_in_gg(x1, x2)  =  gtcA_in_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
0  =  0
gtcA_out_gg(x1, x2)  =  gtcA_out_gg(x1, x2)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U44_gg(x1, x2, x3)  =  U44_gg(x1, x2, x3)
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
partcB_in_ggaa(x1, x2, x3, x4)  =  partcB_in_ggaa(x1, x2)
U40_ggaa(x1, x2, x3, x4, x5, x6)  =  U40_ggaa(x1, x2, x3, x6)
U41_ggaa(x1, x2, x3, x4, x5, x6)  =  U41_ggaa(x1, x2, x3, x6)
U42_ggaa(x1, x2, x3, x4, x5, x6)  =  U42_ggaa(x1, x2, x3, x6)
U43_ggaa(x1, x2, x3, x4, x5, x6)  =  U43_ggaa(x1, x2, x3, x6)
[]  =  []
partcB_out_ggaa(x1, x2, x3, x4)  =  partcB_out_ggaa(x1, x2, x3, x4)
QSD_IN_GA(x1, x2)  =  QSD_IN_GA(x1)
U22_GA(x1, x2, x3, x4, x5)  =  U22_GA(x1, x2, x3, x5)
U24_GA(x1, x2, x3, x4, x5)  =  U24_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(56) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(57) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QSD_IN_GA(.(X1, .(X2, X3))) → U22_GA(X1, X2, X3, gtcA_in_gg(X1, X2))
U22_GA(X1, X2, X3, gtcA_out_gg(X1, X2)) → U24_GA(X1, X2, X3, partcB_in_ggaa(X1, X3))
U24_GA(X1, X2, X3, partcB_out_ggaa(X1, X3, X5, X6)) → QSD_IN_GA(.(X2, X5))

The TRS R consists of the following rules:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
partcB_in_ggaa(X1, .(X2, X3)) → U40_ggaa(X1, X2, X3, gtcA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U42_ggaa(X1, X2, X3, lecC_in_gg(X1, X2))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U40_ggaa(X1, X2, X3, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U42_ggaa(X1, X2, X3, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U41_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U43_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

gtcA_in_gg(x0, x1)
partcB_in_ggaa(x0, x1)
U39_gg(x0, x1, x2)
U40_ggaa(x0, x1, x2, x3)
U42_ggaa(x0, x1, x2, x3)
U41_ggaa(x0, x1, x2, x3)
lecC_in_gg(x0, x1)
U43_ggaa(x0, x1, x2, x3)
U44_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(58) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


U22_GA(X1, X2, X3, gtcA_out_gg(X1, X2)) → U24_GA(X1, X2, X3, partcB_in_ggaa(X1, X3))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = x1   
POL(0) = 0   
POL(QSD_IN_GA(x1)) = x1   
POL(U22_GA(x1, x2, x3, x4)) = x4   
POL(U24_GA(x1, x2, x3, x4)) = x2   
POL(U39_gg(x1, x2, x3)) = 1 + x3   
POL(U40_ggaa(x1, x2, x3, x4)) = 0   
POL(U41_ggaa(x1, x2, x3, x4)) = 0   
POL(U42_ggaa(x1, x2, x3, x4)) = 0   
POL(U43_ggaa(x1, x2, x3, x4)) = 0   
POL(U44_gg(x1, x2, x3)) = 0   
POL([]) = 0   
POL(gtcA_in_gg(x1, x2)) = x1   
POL(gtcA_out_gg(x1, x2)) = 1 + x2   
POL(lecC_in_gg(x1, x2)) = 0   
POL(lecC_out_gg(x1, x2)) = 0   
POL(partcB_in_ggaa(x1, x2)) = 0   
POL(partcB_out_ggaa(x1, x2, x3, x4)) = 0   
POL(s(x1)) = 1 + x1   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))

(59) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QSD_IN_GA(.(X1, .(X2, X3))) → U22_GA(X1, X2, X3, gtcA_in_gg(X1, X2))
U24_GA(X1, X2, X3, partcB_out_ggaa(X1, X3, X5, X6)) → QSD_IN_GA(.(X2, X5))

The TRS R consists of the following rules:

gtcA_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, gtcA_in_gg(X1, X2))
gtcA_in_gg(s(0), 0) → gtcA_out_gg(s(0), 0)
partcB_in_ggaa(X1, .(X2, X3)) → U40_ggaa(X1, X2, X3, gtcA_in_gg(X1, X2))
partcB_in_ggaa(X1, .(X2, X3)) → U42_ggaa(X1, X2, X3, lecC_in_gg(X1, X2))
partcB_in_ggaa(X1, []) → partcB_out_ggaa(X1, [], [], [])
U39_gg(X1, X2, gtcA_out_gg(X1, X2)) → gtcA_out_gg(s(X1), s(X2))
U40_ggaa(X1, X2, X3, gtcA_out_gg(X1, X2)) → U41_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U42_ggaa(X1, X2, X3, lecC_out_gg(X1, X2)) → U43_ggaa(X1, X2, X3, partcB_in_ggaa(X1, X3))
U41_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), .(X2, X4), X5)
lecC_in_gg(s(X1), s(X2)) → U44_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U43_ggaa(X1, X2, X3, partcB_out_ggaa(X1, X3, X4, X5)) → partcB_out_ggaa(X1, .(X2, X3), X4, .(X2, X5))
U44_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

gtcA_in_gg(x0, x1)
partcB_in_ggaa(x0, x1)
U39_gg(x0, x1, x2)
U40_ggaa(x0, x1, x2, x3)
U42_ggaa(x0, x1, x2, x3)
U41_ggaa(x0, x1, x2, x3)
lecC_in_gg(x0, x1)
U43_ggaa(x0, x1, x2, x3)
U44_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(60) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(61) TRUE